AustralieFrV1, Main, Exploration, bibRecord, 006319

Template-Based Unbounded Time Verification of Affine Hybrid Automata

Identifieur interne : 006319 ( Main/Exploration ); précédent : 006318; suivant : 006320

Template-Based Unbounded Time Verification of Affine Hybrid Automata

Auteurs : Thao Dang [France] ; Thomas Martin Gawlitza [France, Australie]

Source :

Lecture Notes in Computer Science [ 0302-9743 ] ; 2011.

RBID : ISTEX:4E7A690E2EEC329283F93F36635B6776134F80BE

English descriptors

KwdEn :
- Abstract reachability, Abstract semantics, Algorithm, Automaton, Concrete semantics, Constraint, Constraint system, Continuous variables, Convex, Convex polyhedron, Cousot, Dang, Discrete transition, Discrete transitions, Gawlitza, Heidelberg, Hybrid, Hybrid automata, Hybrid automata template polyhedra, Hybrid automaton, Hybrid systems, Improvement algorithm, Improvement steps, Inequality, Iteration, Least solution, Linear programming, Lncs, Location invariants, Matrix, Monotone, Monotone framework, Monotone mappings, Monotone operators, Nitely, Polyhedron, Polynomial time, Positive invariants, Reachability, Reachability problem, Reachable, Reachable states, Resp, Sankaranarayanan, Seidl, Semantics, Springer, Static analysis, Strategy iteration, Template, Template constraint matrix, Template polyhedra, Template polyhedron, Unbounded, Unbounded time, Variable assignment, Xpoint, Xpoint theorem.
Teeft :
- Abstract reachability, Abstract semantics, Algorithm, Automaton, Concrete semantics, Constraint, Constraint system, Continuous variables, Convex, Convex polyhedron, Cousot, Dang, Discrete transition, Discrete transitions, Gawlitza, Heidelberg, Hybrid, Hybrid automata, Hybrid automata template polyhedra, Hybrid automaton, Hybrid systems, Improvement algorithm, Improvement steps, Inequality, Iteration, Least solution, Linear programming, Lncs, Location invariants, Matrix, Monotone, Monotone framework, Monotone mappings, Monotone operators, Nitely, Polyhedron, Polynomial time, Positive invariants, Reachability, Reachability problem, Reachable, Reachable states, Resp, Sankaranarayanan, Seidl, Semantics, Springer, Static analysis, Strategy iteration, Template, Template constraint matrix, Template polyhedra, Template polyhedron, Unbounded, Unbounded time, Variable assignment, Xpoint, Xpoint theorem.

Abstract

Abstract: Computing over-approximations of all possible time trajectories is an important task in the analysis of hybrid systems. Sankaranarayanan et al. [20] suggested to approximate the set of reachable states using template polyhedra. In the present paper, we use a max-strategy improvement algorithm for computing an abstract semantics for affine hybrid automata that is based on template polyhedra and safely over-approximates the concrete semantics. Based on our formulation, we show that the corresponding abstract reachability problem is in co-NP. Moreover, we obtain a polynomial-time algorithm for the time elapse operation over template polyhedra.

Url:

https://api.istex.fr/document/4E7A690E2EEC329283F93F36635B6776134F80BE/fulltext/pdf

DOI: 10.1007/978-3-642-25318-8_6

Affiliations:

Australie, France

Links toward previous steps (curation, corpus...)

to stream Istex, to step Corpus: 000E81
to stream Istex, to step Curation: 000E81
to stream Istex, to step Checkpoint: 000738
to stream Main, to step Merge: 006695
to stream Main, to step Curation: 006319

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Template-Based Unbounded Time Verification of Affine Hybrid Automata</title>
<author><name sortKey="Dang, Thao" sort="Dang, Thao" uniqKey="Dang T" first="Thao" last="Dang">Thao Dang</name>
</author>
<author><name sortKey="Gawlitza, Thomas Martin" sort="Gawlitza, Thomas Martin" uniqKey="Gawlitza T" first="Thomas Martin" last="Gawlitza">Thomas Martin Gawlitza</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:4E7A690E2EEC329283F93F36635B6776134F80BE</idno>
<date when="2011" year="2011">2011</date>
<idno type="doi">10.1007/978-3-642-25318-8_6</idno>
<idno type="url">https://api.istex.fr/document/4E7A690E2EEC329283F93F36635B6776134F80BE/fulltext/pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000E81</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000E81</idno>
<idno type="wicri:Area/Istex/Curation">000E81</idno>
<idno type="wicri:Area/Istex/Checkpoint">000738</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000738</idno>
<idno type="wicri:doubleKey">0302-9743:2011:Dang T:template:based:unbounded</idno>
<idno type="wicri:Area/Main/Merge">006695</idno>
<idno type="wicri:Area/Main/Curation">006319</idno>
<idno type="wicri:Area/Main/Exploration">006319</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Template-Based Unbounded Time Verification of Affine Hybrid Automata</title>
<author><name sortKey="Dang, Thao" sort="Dang, Thao" uniqKey="Dang T" first="Thao" last="Dang">Thao Dang</name>
<affiliation wicri:level="1"><country xml:lang="fr">France</country>
<wicri:regionArea>Verimag</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
<author><name sortKey="Gawlitza, Thomas Martin" sort="Gawlitza, Thomas Martin" uniqKey="Gawlitza T" first="Thomas Martin" last="Gawlitza">Thomas Martin Gawlitza</name>
<affiliation wicri:level="1"><country xml:lang="fr">France</country>
<wicri:regionArea>Verimag</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><country xml:lang="fr">Australie</country>
<wicri:regionArea>University of Sydney</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s">Lecture Notes in Computer Science</title>
<imprint><date>2011</date>
</imprint>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Abstract reachability</term>
<term>Abstract semantics</term>
<term>Algorithm</term>
<term>Automaton</term>
<term>Concrete semantics</term>
<term>Constraint</term>
<term>Constraint system</term>
<term>Continuous variables</term>
<term>Convex</term>
<term>Convex polyhedron</term>
<term>Cousot</term>
<term>Dang</term>
<term>Discrete transition</term>
<term>Discrete transitions</term>
<term>Gawlitza</term>
<term>Heidelberg</term>
<term>Hybrid</term>
<term>Hybrid automata</term>
<term>Hybrid automata template polyhedra</term>
<term>Hybrid automaton</term>
<term>Hybrid systems</term>
<term>Improvement algorithm</term>
<term>Improvement steps</term>
<term>Inequality</term>
<term>Iteration</term>
<term>Least solution</term>
<term>Linear programming</term>
<term>Lncs</term>
<term>Location invariants</term>
<term>Matrix</term>
<term>Monotone</term>
<term>Monotone framework</term>
<term>Monotone mappings</term>
<term>Monotone operators</term>
<term>Nitely</term>
<term>Polyhedron</term>
<term>Polynomial time</term>
<term>Positive invariants</term>
<term>Reachability</term>
<term>Reachability problem</term>
<term>Reachable</term>
<term>Reachable states</term>
<term>Resp</term>
<term>Sankaranarayanan</term>
<term>Seidl</term>
<term>Semantics</term>
<term>Springer</term>
<term>Static analysis</term>
<term>Strategy iteration</term>
<term>Template</term>
<term>Template constraint matrix</term>
<term>Template polyhedra</term>
<term>Template polyhedron</term>
<term>Unbounded</term>
<term>Unbounded time</term>
<term>Variable assignment</term>
<term>Xpoint</term>
<term>Xpoint theorem</term>
</keywords>
<keywords scheme="Teeft" xml:lang="en"><term>Abstract reachability</term>
<term>Abstract semantics</term>
<term>Algorithm</term>
<term>Automaton</term>
<term>Concrete semantics</term>
<term>Constraint</term>
<term>Constraint system</term>
<term>Continuous variables</term>
<term>Convex</term>
<term>Convex polyhedron</term>
<term>Cousot</term>
<term>Dang</term>
<term>Discrete transition</term>
<term>Discrete transitions</term>
<term>Gawlitza</term>
<term>Heidelberg</term>
<term>Hybrid</term>
<term>Hybrid automata</term>
<term>Hybrid automata template polyhedra</term>
<term>Hybrid automaton</term>
<term>Hybrid systems</term>
<term>Improvement algorithm</term>
<term>Improvement steps</term>
<term>Inequality</term>
<term>Iteration</term>
<term>Least solution</term>
<term>Linear programming</term>
<term>Lncs</term>
<term>Location invariants</term>
<term>Matrix</term>
<term>Monotone</term>
<term>Monotone framework</term>
<term>Monotone mappings</term>
<term>Monotone operators</term>
<term>Nitely</term>
<term>Polyhedron</term>
<term>Polynomial time</term>
<term>Positive invariants</term>
<term>Reachability</term>
<term>Reachability problem</term>
<term>Reachable</term>
<term>Reachable states</term>
<term>Resp</term>
<term>Sankaranarayanan</term>
<term>Seidl</term>
<term>Semantics</term>
<term>Springer</term>
<term>Static analysis</term>
<term>Strategy iteration</term>
<term>Template</term>
<term>Template constraint matrix</term>
<term>Template polyhedra</term>
<term>Template polyhedron</term>
<term>Unbounded</term>
<term>Unbounded time</term>
<term>Variable assignment</term>
<term>Xpoint</term>
<term>Xpoint theorem</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: Computing over-approximations of all possible time trajectories is an important task in the analysis of hybrid systems. Sankaranarayanan et al. [20] suggested to approximate the set of reachable states using template polyhedra. In the present paper, we use a max-strategy improvement algorithm for computing an abstract semantics for affine hybrid automata that is based on template polyhedra and safely over-approximates the concrete semantics. Based on our formulation, we show that the corresponding abstract reachability problem is in co-NP. Moreover, we obtain a polynomial-time algorithm for the time elapse operation over template polyhedra.</div>
</front>
</TEI>
<affiliations><list><country><li>Australie</li>
<li>France</li>
</country>
</list>
<tree><country name="France"><noRegion><name sortKey="Dang, Thao" sort="Dang, Thao" uniqKey="Dang T" first="Thao" last="Dang">Thao Dang</name>
</noRegion>
<name sortKey="Dang, Thao" sort="Dang, Thao" uniqKey="Dang T" first="Thao" last="Dang">Thao Dang</name>
<name sortKey="Gawlitza, Thomas Martin" sort="Gawlitza, Thomas Martin" uniqKey="Gawlitza T" first="Thomas Martin" last="Gawlitza">Thomas Martin Gawlitza</name>
<name sortKey="Gawlitza, Thomas Martin" sort="Gawlitza, Thomas Martin" uniqKey="Gawlitza T" first="Thomas Martin" last="Gawlitza">Thomas Martin Gawlitza</name>
</country>
<country name="Australie"><noRegion><name sortKey="Gawlitza, Thomas Martin" sort="Gawlitza, Thomas Martin" uniqKey="Gawlitza T" first="Thomas Martin" last="Gawlitza">Thomas Martin Gawlitza</name>
</noRegion>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Asie/explor/AustralieFrV1/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006319 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 006319 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Asie
   |area=    AustralieFrV1
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     ISTEX:4E7A690E2EEC329283F93F36635B6776134F80BE
   |texte=   Template-Based Unbounded Time Verification of Affine Hybrid Automata
}}

This area was generated with Dilib version V0.6.33.
Data generation: Tue Dec 5 10:43:12 2017. Site generation: Tue Mar 5 14:07:20 2024

	Serveur d'exploration sur les relations entre la France et l'Australie
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur les relations entre la France et l'Australie

Template-Based Unbounded Time Verification of Affine Hybrid Automata

Template-Based Unbounded Time Verification of Affine Hybrid Automata

Source :

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri